$\forall$$T$:Type, $L$:($T$$\rightarrow$Prop) List, $P$:($T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$Q$$\in$$L$. $\forall$$x$:$T$. Dec($Q$($x$)))
\\[0ex]$\Rightarrow$ ($\forall$$Q$$\in$$L$. finite{-}type(\{$x$:$T$$\mid$ $Q$($x$) \}))
\\[0ex]$\Rightarrow$ ($\forall$$x$:$T$. $P$($x$) $\Rightarrow$ ($\exists$$Q$$\in$$L$.$Q$($x$)))
\\[0ex]$\Rightarrow$ finite{-}type(\{$x$:$T$$\mid$ $P$($x$) \})